#!/bin/csh -f
make OPTFLAGS="-O3" SONAMEKEY="-R" $1 $2 $3 $4 $5

